\begin{tabbing}
$\forall$$R$:Realizer.
\\[0ex](R{-}size($R$) $\leq$ 1)
\\[0ex]$\Rightarrow$ (\=R{-}discrete($R$)\+
\\[0ex]$\sim$
\\[0ex]if Reffect?($R$) $\vee_{b}$Rinit?($R$)
\\[0ex]then \=$<$R{-}loc($R$)\+
\\[0ex], if Reffect?($R$) then Reffect{-}x($R$) else Rinit{-}x($R$) fi 
\\[0ex]$>$ : case if Reffect?($R$) then Reffect{-}f($R$) else Rinit{-}v($R$) fi 
\\[0ex]o\=f inl($a$) =$>$ tt\+
\\[0ex]$\mid$ inr($a$) =$>$ ff
\-\-\\[0ex]else $\otimes$
\\[0ex]fi )
\-
\end{tabbing}